Contained herein is material that is subjected to copyright protection. The copyright owner has no objection to the facsimile reproduction of the patent disclosure by any person as it appears in the patent and Trademark Office patents files or records, but otherwise reserves all rights to the copyright whatsoever.
1. Field of the Invention
The invention relates generally to the field of design verification. More particularly, the invention relates to a new approach for functional verification of digital designs.
2. Description of the Related Art
The objective of design verification is to ensure that errors are absent from a design. Deep sub-micron integrated circuit (IC) manufacturing technology is enabling IC designers to put millions of transistors on a single IC. Following Moore""s law, design complexity is doubling every 12-18 months, which causes design verification complexity to increase at an exponential rate. In addition, competitive pressures are putting increased demands on reducing time to market. The combination of these forces has caused an ever worsening xe2x80x9cverification crisisxe2x80x9d.
Today""s design flow starts with a specification for the design. The designer then implements the design in a language model, typically Hardware Description Language (HDL). This model is typically verified to discover incorrect input/output (I/O) behavior via a stimulus in expected results out paradigm at the top level of the design.
By far the most popular method of functional verification today, simulation-based functional verification, is widely used within the digital design industry as a method for finding defects within designs. A very wide variety of products are available in the market to support simulation-based verification methodologies. However, a fundamental problem with conventional simulation-based verification approaches is that they are vector and testbench limited.
Simulation-based verification is driven by a testbench that explicitly generates the vectors to achieve stimulus coverage and also implements the checking mechanism. Testbenches create a fundamental bottleneck in simulation-based functional verification. In order to verify a design hierarchy level, a testbench must be generated for it. This creates verification overhead for coding and debugging the testbench. Hence, a significant amount of expensive design and verification engineering resources are needed to produce results in a cumbersome and slow process.
Several methods have been attempted by Electronic Design Automation (EDA) companies today in order to address the shortcomings of simulation. However, none of these attempts address this fundamental limitation of the process. For example, simulation vendors have tried to meet the simulation throughput challenge by increasing the performance of hardware and software simulators thereby allowing designers to process a greater number of vectors in the same amount of simulation time. While this does increase stimulus coverage, the results are incremental. The technology is not keeping pace with the required growth rate and the verification processes are lagging in achieving the required stimulus coverage.
Formal verification is another class of tools that has entered the functional verification arena. These tools rely on mathematical analysis rather than simulation of the design. The strong selling point of formal verification is the fact that the results hold true for all possible input combinations to the design. However, in practice this high level of stimulus coverage has come at the cost of both error coverage and particularly usability. While some formal techniques are available, they are not widely used because they typically require the designer to know the details of how the tool works in order to operate it. Formal verification tools generally fall into two classes: (1) equivalence checking, and (2) model checking.
Equivalence checking is a form of formal verification that provides designers with the ability to perform RTL-to-gate and gate-to-gate comparisons of a design to determine if they are functionally equivalent. Importantly, however, equivalence checking is not a method of functional verification. Rather, equivalence checking merely provides an alternate solution for comparing a design representation to an original golden reference. It does not verify the functionality of the original golden reference for the design. Consequently, the original golden reference must be functionally verified using other methods.
Model checking is a functional verification technology that requires designers to formulate properties about the design""s expected behavior. Each property is then checked against an exhaustive set of functional behaviors in the design. The limitation of this approach is that the designer is responsible for exactly specifying the set of properties to be verified. The property specification languages are new and obscure. Usually the technology runs into capacity problems and the designer has to engage with the tools to solve the problems. There are severe limits on the size of the design and the scope of problems that can be analyzed. For example, the designer does not know which properties are necessary for complete analysis of the design. Further, specifying a large number of properties does not correlate well with better error coverage. Consequently, model checking has proven to be very difficult to use and has not provided much value in the verification process.
In view of the foregoing it would be desirable to create a verification methodology to create high quality designs without the need for simulation testbench and to increase the productiveness of design engineers by minimizing the tool setup effort and report processing effort. In particular, it would be advantageous to abstract the internal details of the tools from the user to make these tools more accessible to designers. For example, it would be advantageous to allow a verification methodology to be employed while allowing the designer to think about characteristics of the design. In this manner, the designer can think in terms of time progression of data at various design elements (entities) rather than the implementation of the verification tool. Additionally, rather than requiring the designer to write properties in a complex and arcane language, it would be advantageous to automatically formulate a list of verification checks that, if satisfied, would guarantee the absence of errors in a design with a high level of confidence. Finally, it would be advantageous to maintain and utilize relationships among the list of automatically generated verification checks to facilitate error reporting and to prune the error space for more efficient run-time processing.
A method and apparatus are described that facilitate analysis of the intended flow of logical signals between key points in a design. According to one aspect of the present invention, hardware design defects can be detected using a novel Intent-Driven Verification process. First, a representation of a hardware design and information regarding the intended flow of logical signals among variables in the representation are received. Then, the existence of potential errors in the hardware design may be inferred based upon the information regarding the intended flow of logical signals by (1) translating the information regarding the intended flow of logical signals into a comprehensive set of checks that must hold true in order for the hardware design to operate in accordance with the intended flow of logical signals, and (2) determining if any of the checks can be violated during operation of circuitry represented by the hardware design. Advantageously, in this manner, the designer is not required to manually code individual monitors for each property he/she would like to verify. Rather, verification cycle time and resource requirements are reduced by allowing the designer to simply annotate a language representation of the hardware design under test with information regarding the desired/expected interaction between components of the design and/or the designer""s expectations for acceptable functional behavior (in terms of the expected state of variables at various points in the control flow structure of a finite state machine associated with the hardware design representation, for example) and the generation of a comprehensive set of checks for identifying the intent gap is automatically performed.